
\subsection{Correctness of SALADS}

Next, we demonstrate the accuracy of the data structure memory
access by contrapositive under the assumption that all the fields in
a struct that can be randomized are accessed from the reference or
pointer to the entry of the struct based on the fields' name or
their offsets. This assumption can be guaranteed by our
normalization component, because when the pointer that refers to the
inside or outside of the data structure instance accesses the field
of the data structure, the field will be marked as non-randomizable.
Here are some premises based on the SALADS implementation.
\textbf{Premises:} 1. When a pointer with the type casting is
referred to the data structure instance, the instance will be
de-randomized.  2. When a pointer refers to the field of the data
structure, the field will be de-randomized to its original
place in the structure. %3. When a pointer refers to the field of the
%data structure, it should only be used to access the memory within
%the field or to calculate the start address of the data structure
%and converted to the pointer which refers to the data structure
%instance
3. When the field has been calculated for its offset in struct
(e.g., \texttt{offsetof}, \texttt{container\_of}), we will mark the
field un-randomizable and guarantee the field access by offset
correctly even under data structure randomization. %4. The pointer
%with the same type of the data structure instance will
% correctly access the field based on its name (. or $\rightarrow$) by
%referencing the randomization seed ($I_r$).
\textbf{Conclusion:} There exists memory access inconsistency of the
pointer to certain data structure instance. \textbf{Argument:}
Suppose the conclusion is correct, the instance should be
randomized. As to the source of the pointer, there are three cases:
first case is that the pointer is the pointer/reference to the data
structure instance. The second case is that the pointer is the
pointer/reference to the field of the data structure. The third case
is that the pointer is outside of the data structure instance. For
the first case, the pointer must inconsistently accesses the data
structure instance with the different type. According to the
premise-1, the instance should be de-randomized at type casting,
which contradicts with the conclusion that the data structure
instance is randomized. For the second case, according to the
premise-2, the pointer can access the current field of struct
without error. When it will be used to access other fields, based on
our normalization component, the fields can not be randomized. It
contradict with the conclusion. If the pointer is firstly converted
to the pointer which points to the start address of the struct, then
further to access the other fields in the struct. In this procedure,
if there exists type casting between field pointer and the pointer
to the entry of the struct, the struct will be de-randomized
according to premise-1, and it contradicts with the conclusion; If
there exists no type casting, it will access the fields by offset
correctly based on premise-3 or by name correctly based on the
randomization seed ($I_r$) , which contradicts with the conclusion.
For the third case, when the pointer outside of the data structure
to access the field, the field will be marked as non-randomizable,
which contradict with the conclusion either. From above arguments,
the conclusion does not stand up, as such we guarantee there will no
memory access inconsistency.


\begin{equation}
\frac{S=(\tau_s)P \in Prog, Type(S)=\tau_s, Type(P)=\tau_p, \tau_p
\ne \tau_s, P\in I_a}{De-randomize(\tau_p, \forall)}
\end{equation}

\begin{equation}
\frac{S=(\tau_s) \& ((* P).a) \in Prog, Type(S)=\tau_s,
Type(P)=\tau_p}{mark\_unrandomize(\tau_p, a)}
\end{equation}

\begin{equation}
\frac{(\tau_p*)(0)\rightarrow a \in Prog}{mark\_unrandomize(\tau_p,
a)}
\end{equation}
%Some acute reader may point out that the accuracy of SALADS depends
%on the assumption that all the fields in a struct are accessed from
%the reference or pointer to the entry of the struct based on the
%fields' name or their offsets. Even though we can not guarantee that
%there are no exception in C/C++ programming, since the pointer can
%access any memory address following ANSI C standard, but in
%experiment we find nothing breaks the assumption. We consider two
%reasons that the struct member address is calculated based on the
%start address of the struct, one reason is that there are paddings
%between the fields of the structure~\cite{Compiler}, it is not legal
%to calculate the relative offset between two fields; the other is if
%the programmer changes the definition of the struct, it will
%re-calculate the relative offset. In practice, we compile the
%experimental software by adding the option ``-fpointer-arith" to
%study all the pointer arithmetic operations, and find that almost
%all the pointer arithmetic related to the struct pointer is used for
%the struct array or start address of the struct, then accesses the
%field within the struct.
%should be firstly calculated from the pointer which points to the
%data structure instance, since the other field pointer will be
%transferred to the pointer to the data structure instance. At that
%moment, the data structure will be de-randomized according to the
%definition-2. As such we prove the contrapositive version there is
%no memory access inconsistency of the pointer access to certain data
%structure instance.
